﻿module AbstractDomain

type abstractValue = AbstractValue of int with
    static member inline op_Equality (AbstractValue(x), AbstractValue(y)) = x=y

let none               = AbstractValue 0
let copy               = AbstractValue 10
let incrementBy1       = AbstractValue 11
let incrementByC       = AbstractValue 12
let additive           = AbstractValue 15
let linearPolynomial   = AbstractValue 20
let polynomial         = AbstractValue 30
let exponentialAtLeast = AbstractValue 40

let lub (AbstractValue x) (AbstractValue y) = AbstractValue(max x y)

(*product has a special rule for as defined in he increments paper, but in loops it is ignored. see paper for more details*)
let prod ((AbstractValue x) as a) ((AbstractValue y) as b) = 
    if (a = incrementBy1 && b = incrementBy1) then incrementByC else lub a b

let prod_for_increment_loop ((AbstractValue x) as a) ((AbstractValue y) as b) =
    if (a = none || b = none) then none else lub a b

let isLinear v = (v = copy || v = additive || v = incrementBy1 || v = incrementByC)

let toString v =
    match v with
      | AbstractValue 0 -> "0"
      | AbstractValue 10 -> "1"
      | AbstractValue 11 -> "1\u00B9"
      | AbstractValue 12 -> "1\u00B2"
      | AbstractValue 15 -> "A"
      | AbstractValue 20 -> "LP"
      | AbstractValue 30 -> "P"
      | AbstractValue 40 -> "E"
      | _ -> "Unknown value"